es:event_system{i:l}, d,b,a,c:es-E(es).
es-le(es; a; b)
 es-le(es; c; d)
 ([a, b] = [c, d]  (es-E(es) List))
 guard(((a = c)  (b = d))) 

latex

Definitions	x:A. B(x), P  Q, t  T, prop{i:l}, ge(i; j), T, True, P  Q, P  Q, P  Q, guard(T), SqStable(P)
Lemmas	es-E wf, es-interval wf, es-le wf, event system wf, hd-es-interval, hd wf, sq stable from decidable, le wf, length wf1, decidable le, ge wf, pos length, not functionality wrt iff, es-locl wf, es-interval-nil, es-le-loc, es-loc wf, squash wf, true wf, es-le-not-locl, es-interval-length-one-one